p:, d:Dec(p). (dectt(d))  p 

latex

Definitions	x:A. B(x), Type, dectt(d), Dec(P), P  Q, left + right, b, True, P  Q, P & Q, P  Q, , t  T, A, P  Q, False
Lemmas	false wf, true wf, decidable wf